package kunsch.demo;

import java.util.HashMap;
import java.util.List;

import kunsch.bdd.AbstractBDD;
import kunsch.bdd.BBDCreator;
import kunsch.bdd.ROBDDReduceStrategy;
import kunsch.bdd.util.DOTCreator;
import kunsch.bexp.BooleanFunction;
import kunsch.bexp.Expression;
import kunsch.bexp.Variable;
import kunsch.bexp.transform.ShannonExpander;
import kunsch.bexp.transform.WeightHeuristicVariableOrderStrategy;
import kunsch.bexp.util.Evaluator;
import kunsch.read.BLIFReader;

public class DemoUsage
{

	public static void main(String[] args)
	{

		// read boolean expressions from folder
		BLIFReader reader = new BLIFReader();
		reader.readFiles("BlifFiles");

		BooleanFunction firstFunction = reader.getReadFunctions().get(0);
		List<Variable> firstVariables = firstFunction.getVariables();
		
		//examples for current variable order strategies
		//List<Variable> orderedVariables = new NoVariableOrderStrategy().order(firstVariables);
		//List<Variable> orderedVariables = new UserDefinedVariableOrderStrategy("b", "c", "a","d").order(firstVariables);
		List<Variable> orderedVariables = new WeightHeuristicVariableOrderStrategy(firstFunction).order(firstVariables);

		int varCount = orderedVariables.size();

		// expand boolean expression with computed variable order
		Expression expandedExpression = ShannonExpander.expand(orderedVariables, firstFunction.getIn());

		// reduce boolean expression with some basic rules
		Evaluator eval = new Evaluator();
		Expression evaluatedExpression = eval.startEvaluation(expandedExpression, new HashMap<Variable, Boolean>());

		Expression reExpandedExpression = ShannonExpander.expand(orderedVariables, evaluatedExpression);
		
		System.out.println(firstFunction);
		
		System.out.println(expandedExpression);

		System.out.println(evaluatedExpression);

		// create bdd from shannon expanded boolean expression

		BBDCreator creator = new BBDCreator();

		AbstractBDD bdd = creator.transformToBDD(expandedExpression, varCount, new ROBDDReduceStrategy(varCount));

		// create .dot file which can be translated to a png image with graphviz
		DOTCreator dot = new DOTCreator();
//		dot.createDotFile(bdd);
//		dot.createDotPngFile("C:\\Program Files (x86)\\Graphviz2.34\\bin\\dot.exe");

	}
}
